\section{Session Consistency by Typing}\label{sec:res}
We now investigate \emph{session consistency}: this is to 
%address a basic consequence of considering
enforce a basic discipline on 
the interplay of communicating behavior (i.e., session interactions) 
and evolvability behavior (i.e., update actions). 
We say that sessions are \emph{consistent} when they are not disrupted by an evolvability step. 
That is, performing an update action does not affect the behavior of active sessions.
To define consistency, we extend and adapt  notions 
given in~\cite{DBLP:conf/ppdp/GarraldaCD06}. %\todo{Do we also distinguish between pre- and processes?}
Process $P$ is said to be \emph{communicating} over channel $c$ if it is one of the following:
$$
\begin{array}{llcllcrl}
(1)  & \!\!\! \inC{c}{\tilde{x}}.P' & & (2) & \!\!\! \outC{c}{v}.P' & & \!\!\!  (7) & \!\!\!  \close{c}.P'  \\
(3)  & \!\!\!  \catch{c}{d}.P' & & (4) & \!\!\!  \throw{c}{d}.P' \\
(5)  & \!\!\!  \branch{c}{n_1{:}P_1, \ldots, n_k{:}P_k} \!\!\!& & (6)  & \!\!\!  \select{c}{n}.P' 
\end{array}
$$
Two communicating processes are \emph{dual} %of each other 
(on session $c$)
if they are, respectively, of the forms (1) and (2), 
(3) and (4), 
(5) and (6),
or a pair of (7), as given above.
Let us write $P_{\langle c \rangle}$ and $\overline{P}_{\langle c \rangle}$ for two dual communicating processes on $c$.
Below, let $\pired_r$ stand for an update action, i.e., 
a reduction inferred using rule $\rulename{r:Upd}$, possibly preceded/followed
by uses of rules $\rulename{r:Res}$/$\rulename{r:Str}$. 
We define:

\begin{definition}[Consistency]\label{d:consist}%
A session on channel $c$ is \emph{consistent} in a process $P$ if,
for all $P', P''$ such that 
$$P \pired^{*} P' \equiv (\nu \tilde{u})\big (E\big[C[Q_{\langle c \rangle}] \parallel D[\overline{Q}_{\langle c \rangle}]\big] \big)$$
%where $R$ and $Q$ are dual communicating processes in that session, 
and $P' \pired_r P''$, then there exist contexts $E', C'$, and $D'$ such that
$P'' \equiv (\nu \tilde{u})\big (E'\big[C'[Q_{\langle c \rangle}] \parallel D'[\overline{Q}_{\langle c \rangle}]\big]\big)$.
\end{definition}

Hence, intuitively, Def.~\ref{d:consist} formalizes the fact that
reductions corresponding to update actions do not disrupt the behavior of communicating processes
in already active sessions. They can only involve parts of the system not engaged into active sessions.

We can show that all sessions in our well-typed processes are consistent. 
This result follows as a direct consequence of the \emph{subject reduction} theorem below: i.e., well-typedness is preserved by reduction.
Its proof relies on a subject congruence result, and on a result on typability of processes within (syntactic) contexts $C$.
%(see the Appendix for a  detailed proof). 

%\todo{The statement below can be simplified to three cases (merging 2 and 3). Do we define substitution over $\Delta$? Also, I think we need subject congruence.}

\begin{theorem}[Subject reduction]\label{th:subred}
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\Phi}{\Delta}}$ and $P \pired Q$ then one of the following holds: \vspace{-2mm}
\begin{enumerate}[(1)]
% \item $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\Phi}{\Delta}}$;
% \item $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\Phi}{\Delta\sub{v}{x}}}$;
%  \item $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\Phi}{\Delta'}}$ for some $\Delta'$
%  \item $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\Phi, c:\bot}{\Delta\ominus\{\rho, \overline{\rho}\}}}$ for some $\rho$;
 \item $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\Phi}{\Delta}}$; %\vspace{-2mm}
  \item $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\Phi}{\Delta'}}$, for some $\Delta'$; %\vspace{-2mm}
  \item $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\Phi, c:\bot}{\Delta'}}$, for some $\Delta' \subset \Delta$ and channel $c$.
\end{enumerate}
\end{theorem}

A proof is in Page~\pageref{ap:subr}.
The above items correspond to %the changes on type $\type{\Phi}{\Delta}$ that are due to 
the different possibilities for reduction.
Item~(1) is related to rules 
\rulename{r:I/O}, \rulename{r:Pass},
\rulename{r:Rec}, \rulename{r:IfTr}, \rulename{r:IfFa}, \rulename{r:Close}, \rulename{r:Res}, \rulename{r:Str}, and \rulename{r:Sel}. 
Item~(2) captures the case of a reduction via rule \rulename{r:Upd}: the exact shape of 
$\Delta'$ is obtained from $\Delta$ by considering the update process that has changed some located process 
with interface $\Delta_1$ into a process with interface $\Delta_2$. 
Item~(3) follows from \rulename{r:Open}.

The main consequence of 
Thm.~\ref{th:subred} is the \emph{absence of communication errors}
for well-typed processes. 
It also 
allows us to prove that every session that is established along the evolution of a process is \emph{consistent}.
We can indeed state:

\begin{corollary}[Con\-sist\-ency by Typing]\label{cor:cons}
Suppose \\%$P$ be a well-typed process. 
$\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\Phi}{\Delta}} $
is a well-typed process.
Then every session $\rho_\qua \in \Delta$ %that can be established along the evolution of $P$, we have that 
is consistent, in the sense of Def.~\ref{d:consist}.
\end{corollary}

%Theorem~\ref{th:subred} allows us to prove that every session that is established along the evolution of a process is consistent, i.e., sessions inside  adaptable processes cannot be disrupted by an update. 
This result follows from Thm.~\ref{th:subred} 
by observing that 
enabling update actions only for 
located processes without active sessions (cf. rule \rulename{r:Upd}), essentially 
rules out the possibility of 
updating a location containing 
a communicating process $P_{\langle c \rangle}$, as defined above.
Indeed, our type system ensures that the annotations enabling update actions 
are correctly assigned and maintained along reduction.
%Similarly, duality enforced by rule \rulename{r:Open} guarantees that only matching sessions are established. 
%This way, once established, a session cannot be deadlocked, 
%as all actions have a dual. We have: %This is the content of the following corollary. 






%\begin{corollary}
%\todo{abbiamo bisogno/voglia di un teorema che afferma che solo gli update "buoni" (compliant?) potranno essere eseguiti?}
%\end{corollary}

